$\forall$$i$, $x$:Id, $k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $T$:Type, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$DeclaredType(${\it ds}$;$x$)).
\\[0ex]Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ (isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)))
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.@$i$ events of kind $k$ change $x$ to $f$ State(${\it ds}$) (val:$T$)